package interfaces;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;

@ImportClass("src.interfaces.*")

@Init ({"getNombre()!=null && getDescripcion()!=null"})
@Inv ({""})

public interface IProducto {
	
	@Pre ({"nuevoNombre!=null #NullPointerException"})
	@Pos ({"getNombre().equals(nuevoNombre) && getDescripcion().equals(getDescripcion()@pre) && getCodigo() == getCodigo()@pre"})
	public void setNombre(String nuevoNombre);
	
	@Pre ({"nuevaDescripcion!=null #NullPointerException"})
	@Pos ({"getDescripcion().equals(nuevaDescripcion) && getNombre().equals(getNombre()@pre) && getCodigo() == getCodigo()@pre"})
	public void setDescripcion(String nuevaDescripcion);
	
	@Pre ({"nuevoCodigo >= 0 && nuevoCodigo <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos ({"getDescripcion().equals(getDescripcion()@pre) && getNombre().equals(getNombre()@pre) && getCodigo() == nuevoCodigo"})
	public void setCodigo(int nuevoCodigo);
	
	@Query
	public int getCodigo();
	
	@Query
	public String getNombre();
	
	@Query
	public String getDescripcion();	
}
